(DEFPROP UNITREDUCT 
 (LAMBDA(R UP UN)
  (PROG (Z UP1 UN1 C1 C2 RC1 RC2)
	(SETQ UN1 (SETQ UP1 NIL))
	(SETQ C1 (SETQ C2 R))
   A    (SETQ RC1 (SETQ RC2 NIL))
	(COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
   B    (SETQ Z (UNITRES (CAR C2) UP1 UN1))
	(COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
	      ((MEMQ NIL Z) (RETURN (LIST NIL)))
	      (T (SETQ RC1 (APPEND Z RC1))))
	(SETQ C2 (CDR C2))
	(COND (C2 (GO B)))
   C1   (SETQ UP (APPEND UP1 UP))
	(SETQ UN (APPEND UN1 UN))
   C    (SETQ Z (UNITRES (CAR C1) UP UN))
	(COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
	      ((MEMQ NIL Z) (RETURN (LIST NIL)))
	      (T (SETQ RC1 (APPEND Z RC1))))
	(SETQ C1 (CDR C1))
	(COND (C1 (GO C)))
	(COND ((NULL RC1) (RETURN RC2)))
	(SETQ C2 RC2)
	(SETQ C1 RC1)
	(SETQ Z (UNITPN C1))
	(COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
	(SETQ UP1 (CAR Z))
	(SETQ UN1 (CDR Z))
	(GO A))) 
EXPR)